package sketch.icse11nier;

import sketch.ounit.Observer;
import sketch.ounit.Values;
import sketch.specs.annotation.TestSketch;
import junit.framework.TestCase;

public class Z_Sketch_SpecifyAssertions  extends TestCase {
	
	@TestSketch
	public void testListSize() {
		List l = new List();
		Integer[] is = Values.exhaust(1, 2, 3, 4);
		l.addAll(is);
		Observer.observeExpr(l.size());
	}
	
	//to fully express the assertion use the following mock object
	public class List {
		Object[] array = null;
		public List() {
			array = new Object[0];
		}
		public void addAll(Object[] objs) {
			array = objs;
		}
		public int size() {
			return array.length;
		}
	}
	
}